X:(), a:, k:, y:( List).
(k  ||y||)  (q-linear(k;j.a * X(j);y) = (a * q-linear(k;j.X(j);y))  ) 

latex

Definitions	i  j , , False, A, P & Q, True, T, x. t(x), P  Q, P  Q, t  T, x(s), A  B, P  Q, , x:A. B(x),
Lemmas	qadd comm q, qmul ac 1 qrng, qmul comm qrng, qmul assoc qrng, qmul over plus qrng, ge wf, nat properties, q-linear wf, select wf, qadd wf, q-linear-unroll, length wf1, le wf, true wf, squash wf, qmul wf, q-linear-base, rationals wf, nat wf